Computers have become highly integrated in the workforce, in the home, in mobile devices, and many other places. Computers can process massive amounts of information quickly and efficiently. Software applications designed to run on computer systems allow users to perform a wide variety of functions including business applications, schoolwork, entertainment and more. Software applications are often designed to perform specific tasks. For example, word processor applications are designed for drafting documents, just as email programs are designed for sending, receiving and organizing email.
In many cases, software applications are quite complex, incorporating many different modules, functions and components, each designed to play a part in providing some portion of desired functionality. This complexity often leads to programming deficiencies, often referred to as “bugs” in the software applications. In most cases, these deficiencies are discovered during the software development process or when the application is tested by a software tester or software testing computer program. Such testing is often time consuming and resource intensive.
In some cases, however, software applications (or portions thereof) may be logically or mathematically verified before being sent out for formal testing. Such program verification may be performed using various known algorithms and approximations. In this manner, a developer or tester may determine that a software application is functioning correctly, or, at least that the application complies with the developer's general conception of how the application is supposed to function. Such application verification often involves the use and/or discovery of program invariants. Existing methods of discovering program invariants typically incorporate exponential expressions which thereby limits the number of variables that can be in the software application. A high number of variables in the software application tends to bog down or completely halt the inference of invariants.